\begin{tabbing}
$\forall$\=$i$, $a$:Id, $p$:FinProbSpace, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$),\+
\\[0ex]${\it init}$:\{$f$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Top$\mid$ $\forall$$x$:Id. ($\uparrow$$x$ $\in$ dom(${\it ds}$)) $\Rightarrow$ ($\uparrow$$x$ $\in$ dom($f$))\} , ${\it es}$:ES.
\-\\[0ex]pre{-}init{-}p2(${\it es}$;$i$;${\it ds}$;${\it init}$;$a$;$p$;$P$) $\in$ $\mathbb{P}$
\end{tabbing}